(navigation image)
Home American Libraries | Canadian Libraries | Universal Library | Community Texts | Project Gutenberg | Children's Library | Biodiversity Heritage Library | Additional Collections
Search: Advanced Search
Anonymous User (login or join us)
See other formats

Full text of "mit :: ai :: aim :: AIM-021"


Artificial Intelligent Froie3fc-*HI£ ani K.{T Computation renter 

Wenc &i--The Prcofsbcsker 


Pail Abraham 
.... . ' • 

-January £&, ipol 


The Frt:cf'ih^tVi r er ifi £ heurle tic-ally tri«itei cCB^putai? pro- 
gram for checking ira^matita! proofs ? w.'.th tb* ftheairtrtE of text- 
tccvc pp^pffl &g it* ultimate e<*al, :ft tone frusta, from esa* P* cc "? 
step jrii-»n to it. a. *orT£sponJin£ negusn-e of fcrrai Etepe, if 
pc.adibla. H peaor&a tha current ttate of the prcof in fcha forra 
of itfat It -56 s=uTJ.'JiJ.en*. tc prtve. There are two Logical Pul*S rf 
iaferenaa; »c*™ power* and iisasrlion (if it i* sufficient to 
prove P N 5^ A i*. a liheorein, tlien it is sufficient to prove A 
iiip^es F)* The peuniBPible fnvwai Ptepa ■■.rilJde these rules of 
infer eu-e as weii as provision fci hawSling definitions, icnaa, 
cB-l^tiiatlons, and revision ec previous state?. A? of now, mast 
of the fortnalipnt, o.?i* pjcsr&wip»3 an* partially debugged, bat the 
heurlatle &Epe-;tr have yet tc. be pro^raimnii* 

* v 



i ?utpofe arid pttLloAaphy ■ * * * * * r * *' * ' " 

II OffsanasatJon of the ?rcof checker 7 

III Logical Po-JErfatloBB of the Proof rtwdur - * • * ■ 13 

IV Th* Poasitl* Froor S:;e*s in th-s Proof eh#a«ep - - 1? 
7 Current Sfcatug and Future Plans 





A proofs heeler la a computer program v:hlch checks watheriiatical 
proof* to- eeo if they ars correal;, k TnatheEr-atJ ral proof is a sym- 
bolic express! on f antf ao can be used aa input data for a "f^rnpitsr 
program vjritfcan in a syuibol-Gr.a.nipul&tlng l&nguage , Now if a 
proposed £roof has been sufficiently formalized, it can be the aired 
by a n*mple set of rules j but if che proof is of the sort that 
appears in most mathematics textbooks t the checking pro^c-dsra siyat 
be ft* Irene 3 y elaborate and even then cannot be guaranteed to worfc 
all the time.: Crhfi~! r .ino; textbook proofs ia the ultimate goal of 
tne Proof checker project, even thoarh it pirobably will not be 
reached, this goal Mli est [>hs direct if n of thete effort?-; how 
fa>? they go rentf'ns to be seen* Some programs have already been 
ch-C-kid out; rrttiiy regain to be written* ha of this writing two 
el^w^fjfcft^y formal "proofs h.ive been chocked.: 

h n -inter of the ideas presumed in this paper arose from 
suggestions made by £ohn McCarthy? however., the vIoyIhj expressed 
hoi.-e are not ne-ieesarily in a^re e [Dent v/ith McCarthy's., 

?herc are two difficulties that arise in demising a procedure 
for checking ccjctbooln p-rcofiK First, the proof 3. are written in 
English \ se-eorjd, they ars ambiguous, inforital, and .full of gapGr 
I am not at present planning to deal with the first problem? though 
it 1b interesting, it is irrelevant to the main purpose of the 
Proof checks project* Therefore, 1 will afisutw that the proofs 
;:hi.ch I wild like the Proof checker to sparine Mill be presented 
in a foraialised and stylised language, but one which makes no 
attempt? to clarify the logical defects of the English original 
from which thej are taken* The Pyoof^hej^er will have to correct 
these defects and check the resulting formal proof at the aame time* 

Essentially* the Proof ohec iter works by talcing each step that 
it it given and gens rating fror it a aequense or formal steps L 
Thus the proof given to it really serve a as a set: of hints on how 
to construct a formal pre of of the theorem at hand. The Proof- 
checker tnurt be something of a proof inventory t&v it mu&t among 




, other things be able lo handle strips labelled as "obvlouo*. As 
the capabilities of the Proof checker increase, It i?il 1 got better 
and toot tor at proving nen theorem In fact, we ttay view the job 
of the Pi?oof checker to be to invent proofs, given a est of hints: 
in the two extreme capes, the hlnta ara either nonexistent or are 
all the utepe of a rorm&'L issd proof.. 

l.'e may consider tha problem from the viewpoint cf checking 
:iEthorta for gene rat ins proofs, lie., seeing; if a proposed Fi*?thod 
of proof generation gsnevatas a p^'oof of a desired theorem. Tha 
two viewpoint** are equivalent; tw a technique which will utilire 
Mnt? is 5irzply a proof Generator with an jnput., Further, tha 
Proof checker H-isfc be able to bkl!£3 use of information on ehat the 
(ceDbsia of a cai'. af.n c^a=;? of goalie expressions are legitimate 
proofs Such a piece of InVori-^ilon is a n-eta theorem, In order 
for any proof -checking ay stem to lit i lice rcetefchsorems, they ia<ist 
bo built Into its etr J:?tiire^ fn the Proof checker , rce t a theorems 
ciay be adder! without- ?hans£r£ * h* overall pattern of operation? 
aarentij:,iy P they are added tc the list of perraiselble proof atepra f 
so thay they act like addltif^ai rules o^ inference (vhieh, inieod, 
they are U 

The Heuristic A pproach 311S ii elatgd Work 

The Froofcbeeker win make extensive use of heuristic methods 
■:":;. ti.;-hi-.3qu^3 . "h:!e is rii-cfizsary became a a tr^.i T.'-.s.f.- r.'.'^-d 3-p-j,rch 
through tha space of ooruv-tctions between snese salve hints would in- 
volve an impossibly l*r£. amount of computation, One scheme which 
I hop± will be useful h?,e will be the ,: Oer.&rsl Problem Solving 
System ! ' of fleuc-11 and E .uz-tu This system has already been ured in 
solving problems in trjgonoraetry, ele inert try algebra, and logic. 
The chief feature of '.tie system is Its separation of probl&ra content 
from proMem- solving rechnJque * jtt mattes use of two principal 
heuristic a: meanF-erda ane^-ysls, which invo]vea knowing what 
rrsthods of attack a]? epproprjate to particular situations, and 
planning which iaveivea consideration of an abstraction of Che 



problem tt hand* Closely r^ated to the fanning heuristic 1& the 
heuristic of modele as Uf.ed by Oelorntsr.. TiIe he- i :iriEtic y for tfcs 
case of plane goetSiefcr:/ r involves drawing figures and checking there 
to pee what relationships hold between tarloup line aecnsntg, 
anglee , etc* 

There is a r>e&ei£flan:<e between the pole of hints- in the 
Proofchecker alftd the rely of advice in McCarthy r e Advice Tales r 
achem^ in each fere, hfj i^nt a DiaohJ.se to nahe use of pieces of 
information given to It r? rorj an external source in ord^r to so^ve 
a problew. In thr* case of . ty.a Proof checker* the structure of the 
*advi<V r Kiak^o it raucfc e.ifJer to rtct armies how tc use it t 

Problem ^tflains 

The * , roofchecrk , e-r will not he tied to any particular area of" 
[jia:--heinatics , although 1 espeit to work mainly on abstract algebra 
at fi:?Efc, Tjhe Proof checker* like the mat hcrcaM clan, is Interidel 
to bo a general -pLirprpe device* Her s. given problem doo&ln, it 
will have relevant thecreiae, heuiMsti£,s 4 a>id tiodel-mkinc rae cho- 
rd yfc. store;! in its ra^ory* Actually* it would be useful if the 
Pi?oof shocker could be aiiari: of ili_ the theo rents It had ever 
prove i n , though it udc,hi have le;sp ready a^eas to those from 
different dom^Inf., The difficulty here Is that thara ainply 
isn ! t enough took iii the cemputerj as things stand n^tt, for the 
addifcio-nal t^eor-ems. 

One poaalble ar^a ef application, thojgn ad wit ted ly soisewhat 
futuristic, is to bhc uftseiwut of lai-f* ey&t*e?fl* The present way 
that one checks r-uch a £;yst-5GJ to pee If St crorfre ia to p^e^ent it 
tilth a wide vsrie.fcy *>f inputs representing both typical and extreme 
taped, and see If the proper output results^ However, it often 
happens that thii ic^thoci simply dca&ii't ^or!^; the system falls 
under podes unanticipated combination cf circuraatari^ag which nswr 
3i;Curred in the tes* •- af pe t One i/ey tc check out such a system, 
however, la to pi- eve that it" worlr^ « Such a proof 4 of course t would 
be inpoeeible for a hufcn to Construct fc*r a system of aven aSld 

coup laxity; but a machine night b* £bis to eonatm-t such a proof, 
iiFiinfl as h*n^s the £t scrip!: I on of tbs- functions and intondsd rao3e 
of operations i?f various floiaponan^a and subcomponents of tha 
syjifcett* And in a prcof atfcaEipt, one rci^h^ ccrae up a'th g.' 
cO'^^terexampI-3 ar.d pcssibi/ ev T e:i sii^jzeifc e rer^dy* 



The Proof checker is organized 'nfco ti:e constellations of 
programs? Wo^hoe. and Verify. In a> Iltion to tho data interna] 
to these programs., Clwre if a list a? theorem, a 13 at of defi- 
nitions* and a J % *t o? ,lo£ltUiat3 prwif .*tep3, Tlw theorem list 
and definition li?it may be a treated with time. verify will 
accept a proposad fonral pr;of step and tietermins If it is correct i 
if ths 3 tap ie cornet, Verify will d:> ths necessary updating of 
fche state of the universe, Method will tie t ermine what th<2 next 
step should be; it will make its a of nhe hints given as input in 
finding this step. The steps tehich Verify Bill accept must be Jn 
Bb&ndsrdlzed form? thus , all of the heuristics ara in the province? 
of Method, though Verify will hurnJl: updating in such £. teay as to 
rea^e the- u.eo of hourie bice easy* 

The current stats of the proof 13 recorded in the form of 
what it is sufficient to p;?ovo* We will call this expression the 
CLifficiansy, i,e., at each stage It iu sufficient to piovs the 
ftufficlency* Then Ir/tially, tho sufficiency its the theorem wa 
uistt to prove; arei Nhen the sufficiency hsa been reduced to T 
{truth), we know vs have proved fchs theorem* Wb nay record the 
tuff icier cy at various stages of ths proof sncl refer bncif to it 
later, oo that If r,s conduct an unsuc easeful aubprobleBa exploration, 
ve :3an return to E.n earlier siabproblerc ivithznit havir.a to repeat the 
Initial stops of tbo proof* 

This particular foiw of recording - ne iurrent situation is con- 
venient because of the uids variety of logical s true fur as which may 
appear in a theorem or in it& p?ocf* "0 use a list of hypotheses 
and conclusions would ba aukw&rd, for instance, In handling an if- 
and -only- if thaorena, unless ilr were to be broken doe:n into two 
separate theorem* • Yet Eu^h theorem;? are often proved by a sequence 
of bi conditionals > and this natural sequence can be retained in the 
sufficiency forir-oiaticm of the proofs Further more, this formulation 
aaliK-a backwards proofs quite easy to handle, and they ara per hips 
the moat nature! kind, Afc the tf&iae time, It x is possible by using 

certain logical taut qloEi.es- to icake forward proofs; and the 
TqaC'tilnsry for hanlllng Such ^roofE oan b-2 fc.il Ifc into Mofchod irt 
sueh 4 WE.y that the u&er need not be a;sa.ve of the few complications 

that this entails- 

■■ ■ • . ■ . . - . 

The Theodora Llet 

The Pro of checker in endowed with an initial get of theorems 
which are placed on a tli^orem 11a t„ ani each newly proved theorem 
Is added to this 15 at. t^mraas proved during the course of pravinE 
a theorem are also added to Ihis list. When-aver a theorem ia 
referred to In a proofs it. is btoucht to the head of the theorem 
list j so that frequently u^ed thacretifc are ennily ac c ass Ibis « 

Each theorem consists of a nam?, a list of variables t and £ 
forjtu Whenever the theorem is used In a proof, it Is referred to 
by narcsj the va^ifcibles designate those elen>snbs In the forci which 
lt.:^ b^ substituted for* We z?s.y think of the variables as 
designating an^.vei-sal iiutntlfiers which I implicitly precede the 
forra so as to convert It to a th^orew in the ordinary senao. The 
form is the actual statement of the theorss; no inhjarsnt res trl-t ions 
are placed upon its foriaat, though for any problem domain, the 
format will be specified. 

The Cefl r ltlon List 

The Proof che; Iter aim h&e available to it a list of definitions, 
A proof r.ay bs interrupted at amy point to raaUe a new definition* 
A definition is a Imply an abbreviation, with provision for sub- 
otltuting- for certain variables within it a Each definition consists, 
of two r-ames, a list of variables , and a form. The reference nacig 
Is U&&d when, we refer to the definition ir a proof step, and the 
Internal na^a is the one actually recorded in the sufficiency and 
in any theorems or. the theorem list in which the definition ia 
used^ The form ard variables operate in the sane way as the form 
and variables in £ theorem. DefinllimiS, like theorems, are 
arranged ao that recently used definitions appe&r at the head 
the list. 

■ ■ ■ 

Th.-i Need for Two Faroes 


We need two narca-B in a dof Jnltion because etheruiae we way 
accidentally assl^i to & definition a re revenue nrne whith already 
I133 a meaning; and then >y riiklr^ use of the definition, ws nay 
make e false atep »-:hith vrill p?>hf ^'r^rf-.U Ar, —iewdIs 7? ill 
illustrate fetis danger* jiftpMe now that we have cii]y one name 
aepioclafci;d wiC-h & definition* Let ue define AJ!D with varieties 
X and li as {NOT, (OR.. X ? V? > n Tbtia AKD iq the raws, Ol, Y) it the 
;lrt of variables, and ()3GT, {HR r a, ")) is ths fory& T Sew uuppose 
Fiv^t ue h&ve as theorem (HOP, (OR. t, T)1, Shan ths theorem is 
the original s uff iciescy, By ualng the d«fini felon * we may then 
get a? sufficiency (AND, T. T); and by other Fjaara we loay reduce 
thin to !?, ThU3 ws HOUL(i have somehow prevented froti: entering the 
AJ3D Into the, Buffl&iency li! the above example, we would not have 
bean sblu to carry out the proof. If an Internal natsa- say GOOOJ, 
hat. been entered Jn p'.ise of AMD, we would have had as sufficiency 
{GoGO^, ?, ?), which won! id be unprovable a 3 nee GO003 hag no Vrr?:"^ 
propel tl^y d 

In jjensrLx.lj too u.i-e the raferencs n&i3ie when tie refer to & defi- 
nition in a proof, bv.b the internal n&ma it the one actually re^oi-der 
In the sufficiency. The Verify prcgrarc handles the "substitution of 
■:ha internal nafl^ for th* reference mrae automat} eally,, Hhrr in- 
ternal EfiiKto ic a newly" ^enar^ted aym'jol which can be guaranteed not 
to have baen uaocJ for anything bsftre; the progrs-7?! which creates 
i:ur.h eynbola lit l£$& is c-ajled Usrioyn, The symbols, it gens re. tee are 
of the ft.ria Gxxxk, vrht.ra tha j: r s a^G d^cir.ial digits ^ 


It 3a possible to redefine a term 5/tr. though. It ha& previously 
been defined, Itti-on ws cic thia t how-aver , vo lost the ability to 
refer to the previous definition, This is hacausa whar. me eearGh 
the definition JUrt for the reference riaise, wa will always come to 
th^ later deficit len fir&t; and ws can ae^e-."^ a definition in a 
proof step only through, ite reference name^ This le as one wo aid 
:ika It to bai for St permits -^ to- make teTRporary definition? 


of tense: without presr^diia ths later us?e of ths^e tortus for othar 

purposes. The interna; 1 . r.aiTi^r of tho auctee-alvB definitions will 

remain tniquey £o thr*re la no 3«n£er of ronfislori, 

Often, f.n a he uric tin proof, tfe toil J Bake steps tshloh, rihila 

correct, don't help to prove the Lheo^eig. Sir±«e sueh steps may 
actually lead us to a r} tuition uhere ths suffis'^ncy la a fal- 
sity {&r*d he/ite t&iprovafcle ) , we emefc have a May to e° bash to 
pr-evtoiia suf fiajenoies.. At th*? same- tljae^ wq ^o^ h t want to fcssep 
all previous Buffi^innujes, because it rjay talre up too igjoh rocra. 
Therefore, there are tifc ways in which we nay nave past 


YJhen We il£tre a "tap, *ie nay request that tfc-j ^ast sufficiency 
be preserved^ V't ns; 17 gi-ln R<33 eg 5 to :S t t-y reverting one or more 
times, depending on how fp7 a] 0x45 va have Lioved subasfrjientlj . 
Tr.ere It a parameter^ set by Wa^hoA, which tella Verify whether 
or net to preserve ths most recant tuff ivis-nay, 

Tt.a list of FjL T e_a_ejryed- jkib problerciE. 

The reverting p^oc^dturji is no-: aj^uafce irhfcjj we wish to bail: 
up several step?*, move ciff in aiiothar direction, and then, after 
the r-ew exploration proves feasible, return to frh^re tje started. 
It 1e inadequate be^auflfc th* starting point lies on a different 
branih of the explorer Uw tree. ;{n order to handle this, there 
Is provision for naming the eurri-n!: sufficiency at any tlras find 
storing It on a list of auhproblero to be preserved. At any point,, 
we mey reattach it if we: *j±fih„ We may also r-cmeva any a off id en-.: y 
from the ltat of preserved QubptPOblenSr The items on the list or? 
preserved aubproblenfi are then aoceaiad by their narae . When tha 
theorem at hand h&a be*u proved, the list of preserved subproblems 
If eL-t-onaeic&lly Glfi&rad, 


Ea*.-h tyi» or proof etcp Is 1 rap**j*ent*d bjr & program which 
taker ths parameters of the step as 'r.pul., updates Khatsye? needs 

to bfj u-jduttd, and £.-v^ at output" T or 1'. d op 3-; lino; on Heather 

or not she proof otap 1b correct. tfrtati (■■wis tr,sy toe incerpovatid 

into ttto system If they ire sat up a& pace of etepaj crdlnsrilyj 
they will tel:-s t;ie aaff.'^enay at as input , test it or a gutajt- 
ppeefllon of L.t for a Et&:*tiful£r prcptrty, ar^l rberi trEnafariE It 
in acta* uay L ]*q.' 2 list ante, £ 1o£I~el elc^lifijtUioR program would 
correspond t-o b jestathsoreEj ru;l"! a pro^sa racjj.d red^c the 
sufficiency to a ei;:^1#:? tuJ: logic ttlJv eq;uI T , ajLant- ibrci. The 
actual raatatheoron ts?uirt be £hat Mis rssi;!: of t-lmplification is 
*n a very case lo^jfc&Uy a^eivalsftfe to vha original, forra. 

?»- j- V' erj.fy ?| 1 oc;j^m 

Tb/i Verify vTrogr&S] . tp we hat;c po^n^.i out, ciitckB each 
successive ftsp of the proof, and perfoi^ui: various k^nda of up- 
dating* Before exEBSiiaine any eteps, it etijigns internal t:aro5£ fcc 
f..".1 the variables p.o as to avcad &onfXi<strr i-;Jth preuto-jsly aBPlgned 
Ckan?J^i: L Thereafter* when v^riLbl^a are referred -to fey their 
ffcK&F, Verify raplAasn 1;h#BS n£Pi33 with Lhj internal names jjn the 
eteps* of Hie proof., V;i-:e ir.iithtd nea-i no : e T jen be autare of the 
existence of thoce iriti"ijal ns^ee*. UFarllv also asts tha 3Jfficic;niy 
inJilall.y to bo zht theorem wt v:ieh to prt^i; wh^n thfi khsorarn h^a 
been proved , V*fify pln.cfc- it s.t the hear? t>£ the theorem list. 
Verify repeatedly calls on Hstho-l to ppodL.'.e a prcof etep fl Each 
pt-ooi" slop it in-Heated b*y the r-fi" 1 ^ of a p;^£rari> sr.d- a get of argu- 
ments for tht,t p?cgr&n; , Verify ^hacliP fchf\ tfro prograra nairis i& on 
the list of iGgljjircaiVe proof jstepa, and, jf so, cjp^rat^s t;]i^ pro- 
eraoii ?ha ri:Suli; irKj3.T;:tes whether or not the step was o/orreit; 
the proof tU-.p pro&rara ]]andlen the up^citir^ th*it needa t-o be done.- 



T]i3 Method ProfTafn 

Wet hod 1? called iipon repeatedly by Verify tc furnish pre of 
steps.. IfJhlle Verify will prob&bly reirj.ln unfihin^d £S the Proof - 
oheclcer is piodHfiefl, itat'.-ujd iciii be highly rubiest to chants. 
Method us as hecriatj.c isathods, in general, to determine what the 
next proof atop should be. At present, Hetfrod air.rjly feed* the . 
Input directly tc Verify, but this is onijr in order to check out 
Vsrify, As wrar-k progresses * Kathod will bscoBia ttore and Lr L o?e 
elaborate , 

Qna possible way of elaborating Method it to 3o to hierar- 
ofri^ally, R^thsi 1 then reh"?5.t£ Ketlt?i tc acoounfc for hsw lnprow- 
casnts* t new Method would by written which uses the ojd ons as a 
subpposrrii?. This technique is well adapted %a heuristic progparas. 

F tela of Condon g u'o g* pr J s 3 i_or g 

In eucesseiv* sufficienc-is^ there will often be Urge sub- 

expr&SBio:rjE which &*£■ carried elc-ng intact and er j j therefore 
idsnticalr The Proofcheo'icer ha? b^en tr girt:, zed £o aa to have both 

sufficiencies refer to fcha sai*i2 ropy ^f such a subexpression. In 
gonRral, copying is t^oidil as much a» possible, stvlns storage 
and time* 

Tuis might appear to bs merely a pracsirjai programming device t 
but it has an interact ins counterpart In ta;^booV cia the mat led . 
Ea^antially, ccrarson pubeipraoetons not like pron.o^inc; thny are 
useful in the sajoe way that it is useful in a boo.c to write an 
equation, nurab=r it, ana later on refer to i.t by number. If mo 
did not use the numbering techniqje op its equivalent, rfe would 
have to write the equf-tion out in fun whenaTsr we wanted to refer 
to it. 


Vs will etart with £ siaes or pairs ^j*^) for * = £/ £ # - - i 
which we shall call Iftifrlal tLeargflg » K&eh T i is a ayutoolic «.- 
preE£lon;ea<:b B^ is a £«t af at^TJ-fl Eymtols ctr^Mia* l "* '^In J 

V* refer to ^ &i? th? fcjriL of ttiie theorem arrt to '.hec^, as the 
vs .frii.tles of the thsoran*. .tf jj ^ P ■_ 2 P *♦- r u-^ are eyrc-boli-i ex- 

pi-ei»t:ionp, than the result of putytitJting ^^ for^i^u^ for ^g* 

,.• , u ]c forct^j, Jn ^ iB a theorem i nat&nge . Kt-i L e that the T^ 
■ k 

are thtiorera- ine-Kinces ty the jfl^n-ifcy substitution. 

A proper tyl^cs gyaftol is att sialic symbol l?hl£t is used solely 
sr a variable in a theo-rer, and for no o-'her purpose, For inatancft, 
&10 and PSAISE woxld not be proftrfcylese symbols* In LIS?, the 
function GEK3YM In used tc triage these symbols. 

Ie~ 5_ bs a symbolic axprc&n? on, and HippofiQ 1:hafc there exists 
a fl^juenoe of sent elites S,, 3 2 , -,• , S n F-^ch that 5^ — S 4 /;. = 1 , 

2. , -. , n) and ^ is the eyntol ,: T'\ (The neonlng of *-* will be 

explain .2d shortly; T reprttents troth.) Ish p^PU, •>« > & m be * 

fli:t of prop«rt^lee£ sy^jole, tnd danote thlG set ty^. Than 1 ha 
p^lr i&-, r V) i- a nLeorem P-jrthsrn^re^ the initial theorems are 

theoz-nin;- * The class of thsoz'eire if tKjs forced recursively, 
tarring with the initial theorems. 

We 6eaot,& "i" ia a trhsorent inKs^e' 1 by - s.« an J tt it is 
sufficient to pro re P'" ty *"J 3., The logical ays'eni IB baRfcd on *:wq: 
riles of Inference* 

1. If h T and -t S, then -i T"iS. f Insertion rale) 
3, If t-5^5 1 and -fS*,, Mien H?. (Modus, ponens ) 


- A - ■ 

jnt.-'j.it^ftjy* £ ~- F [ m*ann -f S ^ -/P 1 . Formally tte say 
S,«- S [ if and onlj- if 

■" - L S ! lis of the form Tr*. 1 ? and f- T, fir 
•:.«-. E, /* S l :??, or 

J, S' 1b obtained froTi S by substituting for foms eabex- 

prappion of S the equl-Yr,lsnt of that &jb express ion, provided that 
the auto evp re Eaton la ; L *ot part cf a quoted eubejcpreasion, 

Eo^ vacant subexpressions are of twa types; 

1* ft def Inad tenn la 5 qui v slant to thai; Khith It def< naa« 
£« An exproaeioii i.;hich r spree gli^ tha raeaiL: of a calculation 
IP eq\A5, volant to the : ii e&ult itself." Fhe calculation ie p9rfoi*Ji£d 
F;y evaluating the expression ajad then replacing it by the quoted 

reauit of the eva^uat^on. 
For instance, 

ttoiQd be equivalent to 

(QUOTE, £CGH3, (?, [A, B)})* 

Here £UB#T 1e a LIS? function which sjh6titu*:ss its first EirfciM&nS 
for Itc second ar^upgnt :ln lb 9 third argura-irit r 

1:he lefinltior; of — 3 a .? hanged vjberi, mfrtatlisarsTrE are .added to 
^h<j sjietufj-i Eherafcre, ;he above description corresponds to the 
»y&feera arc it now s^a-i^da, but in ry»t perifoarxiRC T 

Role cf Initial T'.^'sorece 

■■■Tie initial theorems differ from ejeioras as we think of thew 
In thfifc Cor H^st preplan, detains fchere is no effort to snake t-hei.i 
non-rodu^dint ^ By ual^g a system wjtli a lar^e initial endowment, 
iri;.ej?rj5t!.ng result: 1, sra raa/hed more c nicely. It Is true that all 
of esa'jhe natlca may bis constructed from lower predicate calculnc 
with identity; bat the working Gathe3tf.ti.cian clcss not ordinarily 
ral^e lee of bills fiLf;t, even tho^n he la aware of it* This is as 
true -."or t^po„ogla.bs arid algebralaleU. as it is for hyvSrodyr^mi^iet* 
ar.1 nimri-ml analysts, even though the former may occasionally give 

This page is 
missing from 
the original 


h,; he Varmnt of the? Calc ilstl^n R^e 

In psr-crj.UUiR t*e cuictij atiari r-.il 9 r we have 1st the wolf in 
the door. Wo voulA life trhs Froof^haslcer, when g*ven a proof, to 
te fuarfikTitaed to ^.vt? ui ft vordiit- However, whan wo j.hfcrodus* 
t-hfe G&lGUl&tiior! r-:;.e, t--J cefl. rto ledger guarantee this, except at 
great coE-t. FG* whsm w-i ceietrt acme gutsxpreaaion of the sufficiency 
ar^ci proceed to da:- f-iilct a iia v&lu*, fcii& ealiiiliitlori ir-ay rot ter- 
crtiAte; furthermore p U f.B in ffjrt'rAl '.K^r»e?ibl^ it protest the 
sut express ion to see ^hethir r-r r.ol liie eal^ulafclcn t.ill r-n wild 
?r: aors X&T.B& art;? d^f/fr^ t'-.t; Proof r^n^e* 1 prc-gratf or r,c?Jify its 
sonkents , {A fantastically ^lcvar j.aarj:ir<£ prcsraw, for infrtante, 
iiwcht ie;irn to eh*iat by tnodifylng she p&rai&iesGrs of the Proof - 
-he-L^er do &? tc Tot'-s i'r to asso^ fal r .s ^epai; J iho»-i problem 
may be skived by running all s&I-rolatleK steps «i fin Interpretive 
b'arSs, bat this requires a yrl /&.te and <juite elaboraU interr*eisr 
Per tke ?roofchca;jst»j fu^tl«eru!ore, it w^uld be jJHfco&Fa£ly !rip*e*- 
consuming because i3B.ahin.*-i&ng , 'irLfre progrSiaE at t*&l^ EJ9 higher- 
^e*'5;i-- ! a:'j ( g-j££ J r£ J ' praj.;:^^ '-.oiiid h£"t; te bo interpreted 

r ?hi:* diffiri-jity la ;-:&r*died by placing ail calculations imdor 
the control ^: a program rat'ert Errorccr... Errn^et causes meat; 
detected errwffts and .'.orj- ! eppiJnatli^ c&ic-jiatieh* to return to con- 
trol to 1 -ha Fx i aafiihettfc'7r . It raili net £?it-V(i an pu;:t, arrorf*; so 
;h:l.g loslstl jLoapbaln do?? rsrta:n, Eowysr, defective proofs Khlah 
do get by Error 35 1 tflil ardi nar3 iy c£P5& Hie ?»&■*> fuhtM^er to 6 top 
richer t^an to ?£v-5 & fa~'?.3 ail^Y^r. 



Wrien Verify rs^e-Sv^s a proof step flora Method, it checks to 
sea if th* step Ss of on? c? th& rsict|."C«^ tvt , ^i J &^G has the 
appropriate svitfr-er of parage 1 , ctt ^li:-h 5 t . If" rat , *he step *e 
erron'aaus, If thece ?:i3tai*ia a?a j&ef;, t > : & ti^re o:* Vr-.c i:-,ep ie 
fasten as the r.^irt of ft fjan£iJLcn, a.nd Mna pir&iT^t&PS of the c,:&p as 
avgiunsjnt? Pf U-.^t Fuiw.fclott- fot- ei! , >r hypo of step f she jorKv- 
Erp^hdlRg F'.ino 4 '* on LV}ic-. n it? the !?-tcu ».c foe i.f f it \G .■ , :0.. , ?'3.;t Ahd, ii 
£lv, £■?-£;■ tha jw-s^ssery updating 1'r c function i? tfuleti by Verify,. 

The typas of prf.rf ^tspF have tet.'?. e <j Ler.teci fer rJie.'.r uris- 
fulness a? pf!miri<;ot : - or* bit-LId^ng-blc^lts is coiiatfjtfv.ifijv T-he r:yp*:£ 
of r 4 . sp* w are rea.^y 5 1*^ row ted ift. Th*? £*$; r&ol all ueefa2 by 
fr.be pp a?, vet? . t*- v, eve _*■ , v> ; « -, ^. & i i xi £ l-c jpr a .id -lX; fcfc 3 n i d hI tl: r^e r ta I ft 
ffpa?4flr theoreiffi, rtty bj'jol-5 =jui":E ptf-tsrilll. 

The- fc;:ir>tffa# step.* art a¥ai}.B*Xa a* freyeut; 

tiii ti pl'ep lass a? par sine ?>arc She n&ws of -a theorem 
and a 1 5 k i r.f p i A h t *. ? i* c i c na . T he c or \ ■■& s po r*3 ! ng f utu* ti o^ 
finds t>>e theorea on the theorem D.J'-S - . perfc-rras. the i 
ind icat e d ?, abn i i t u£ i t n"? . and t h en app 15 m t ! "ii - ^r a v t if: r, 
suie io the resulting. xhaor*i3 lr.jnan:o a^»1 tfca curr^n;; 
ft uf fide-nay. if tha n?ise(3 tb&orein r,s wo 5 on the* thsoren 
Ii.et, or if th«; variatifts r .r- fciw etiibstlt it'^cri r-i*'t do 
not corre^-jO'M ' z.- t'cs :^r- i*5j.s:.. c? X'r.s C'.eotcin, the step 
is redacted, 

l^^s e^^p h£.a t." parameter tin-. naiEa of s theorem* 
The correspcnii^JiE f^msticn flr.-i^ tl-.e Theorem on &hs 
thaorais li-ft, ^etermjnea iht px-npei EJbititutiOTW for 

th& Var^sait'S tf tl*e L^eorena,, p.n:l v ,h.?i sppii^s ttj& r^it 
of r'ttt'BrAB -ipiup ponena i-o t?ie ;'-e iUlt ;.n^ theorsrn ard the 
i ui re n f, & ■. if f i .4 :: eh; j? k Th ^ ■-- \ & x ■■ -.-■ \. i ;-. b:» ?v- jes t=ed If 1 1 o 
nutae'd ^n?orere ;' ■? nor f^n :i e '^-eoresr. H?t, cr if t.!i* ther-.^ 


t/.r. nat c.f the f'pr.i (Ih'ME?, antecedent, eonsffrijent 3 , or 

If She sufficiency "* no* a fi Jibuti tut ion i*istan.%e of the' 
nonsequent with reject to tha varieties of '-he theorem . 

■?hla step faa a* arg'itier.fc & lt*t cT A's art4 D ; a tfMsfc 
indicate the. a ufc s K.pr e * rr .1 en of fcfro c i-f t* J - c lc *>;* y ft her e va > ije 
is to be calc^atsS. If the i;.Fb Y.&h r,o alMfehia, the 
F'jbexprefisiori is the entirs entprsfcsicn* T^ie rt-?p rap"ia*i»G 
the nubexprevfiScin * ty Li at (QHCTE; #val[/]l* The &fcep 
will be re Jet to-:! if the list reaches nu ascitic symbol c>i H 
a quoted exprtt-sicr, po?c;'<» :; ^ &\hi;-;y ;.<M . 

Mr.is step hat af- QrjTMLnjiit^ & na-^ r a 1'tl of ■,■ ariaV Isj ± 
and a form. »?i th.f. =s ?^pp T t.'oe ?roc^cher-.ker in used 
recuPfi'velTj £o eh^u the proof of a lemgta, ahil? ^ erupt - 
rarily neglecting L.fce? main tr^crem, XV rhe APin^a ia 
proven ; it le added to the zfczor&u list; in eny caae T t oc- 
troi 1? ret-iFTW!- to the prccf of '.he Ttsain theorstf wh*f: 
either the ieaac-s ia proven or th? r -r oof ghee !/er ia is 16 to 
giv* y$j m it, 
5, M&kedEf 

Thi.3 Siep haa as ar^Juanttt a nams, a list of variables, 
an^ a for©. The sorrespenaing fono#ion firs', assign? an 
interna^ nzuae to be th-3 equivalent or the TT& France ri£it:e. 
It then pla.ics the list which contalna bo^.h nsnsss, the 
variables, , ejfot the for** at tr.e begjLnnin,^ of U"j*s tff fir,' t:. Oil 
116 1- 

Thir. Siiftp Ivf.i* af parsmster^ s, r.anrs ani a Hit- of A -a 
ani D'ji„ Ths A l 4 F4^ D's ar£ ur.e:l r,o indicate a Ruhej.- 
pref.ft5.on of the &uf£loIejrKj7: the name ^a Vhe re f trance 
narje «r a i^firjl.tior, . ?'!"■«■ a-orre^j^nii^^ ^unotien ^e^i 
i!e 3e'fir.it1rs:i frnm J-.h? i*firj;icn ii*v a^.? cha^ir t-.ft* 
■j-.ilr-exTjref'.sicri to ree if i. :3^ & iat:-;it,jtion intt.pr.-fl of 


the fann of the de fin iti on< It 1 ?"^ it t-c-;-j ;i;aa sh* sut- 
ejpression by ti llss nfoose first alftjaar^ i« rhe interna'- 
narao- of the definite ce, ?h^ remitting elements haire the 
property that ;,f thoy are maiihed sequentially with the 
variables or ?.he difinlfc'on ami nuLft&ltu&M for ther*e 
variables 1'^ the forw, the result Ifl the original 
T* yn-Je f * no 

Th', P E-.op hf.k as paries!;, er a 11 it cnf A F E anl r c & 
Hhigh indicate e. sutcjipres^^rj of the ciffieiefisy* The 
first el^Btar-fc of this :i:;!l.e:':p:r5B'iiar[ i^ t&'Ken a# the !/■- 
terra! nacre o" a defini titn, an;t che definition list is 
bsarehed for ^at naore. a oatatAsution llFt* is fora,-?d 
by na tubing thf- euacesaive alercents of Bhe subexpression 
with T-bs v£riabze:i cf the definition^ an 2 then the 
indioal-ed a , jfcst,s.t ation* ors performed on tbo forra of th-j 
definition,. P:.nally J the 5 Un Repression \c. replaced by 
the result of this substitution. Ehe step is Fixated 
if the naKe^l d^fiuitioa i* not &n the definition list, 
or if the number =f e!i agents foMo^'.rj^ the internal name 
of She "tef'n.V^ott in 1-ht ^-iiic-yp:e j >fien Ts-nat a^ual to 
the njr.ibor of \&.rifctlt:3 ci' r^ euberpre salon. 

Th; 1 -j **>ep haE af ^r;; no '. 5T & reference naine . It 
causes *-: pair fhees fi?rt oleisent is, the na-w and Nftose 
Teccrrf els-^n', i* t?.«e a arrant- sufficiency to le pla^d an 
the list of prefe-srved JEUVprfltlCMl, The aurrent BaffieietK? 

wll] he- aMe to be itohvOt-.sj .Vf n^i e^E^ry a 1 ; a later tiTis-. 
9. fiea t_t!i^;j![ 

"h.^s step has a?, parameter ttie raraa of a 5 ^bprofclera 
on ih« lis? of preserved &ubpret lecig- ■ X~ causes the 
current auff'iclensy to te ->et to tbe- & L jf fiaien^y psire-3 


wlth bhe gi.vari nana on (h* Ms 1, of prt'atrvecl nu^praMeas.. 
Eh? Etep is r£js<i:^c-rl XT the naius <5ois imt cor-Fo-spojvl ic a 

Tiiia ;jf.?p har- at pa 7 ir,:c-l,ei" the iniue of a prokl?m 01; 
the list of prefer ved su'.-prfti.leJHS . ICt ea;j.£i?£ that s-Jb- 
pjroblem tD bs csje'ied frcr- the Iijt v 
11, jp-j nath^ g 

^riift Et;en has nc parsi^ters, .and has ito effect 
fchatsotrer h 
IE. geygrt 

?b*p r.i ep ha^ nfl parar.L aer*£ . It cfcUf.en as to take 
tir.fr aer-OMi nott recent. &uff,1.( J.-e.r;Cy a*? thy Current 
eufficiewy* If tte ruirent sufficiency if the theorem 
we wish tr prove, Uj-> step If.-. itst j^steeK Ifoleis the current 
&ufflcisrjjj it? sived ty a riE.mepr>: f a revert trill C2 l ^-e it 
to be Loefci 

*£hi& ?iie|i has n^ par&rae^erft. ."Lf the ejrrsnfc s.tfflfi&n^y 
1e "T", u* place the th&wea .if, the It's* A of the theorem 
llstj Rnd Voril'y will return with Lrt ans"*? of Ti If tihe 
eufflalenoy 3p r^t- 7 r t-hfc s-.ep 2 s rejected. 



: -^'-i 

llf of this writing, the Verify p-rot.ran is In the process a J' 
debugging, and the- PfeShod program i* in ifce ime' riwli merit ary fornj 
. Kethnd merely tfekes a List of alepe, peel* them off one by one, 
and pfifses than to Verify, while print irig o^i; useful lnfonEition. 
the ppogrram has teen co3#3 entirely ir: MSF, which seems to te 
well suited (re the appjieaMon. Jr: pi&irtirtii&r, ifca handling of 
i^otaaon subesprep^onp without raneiie&s&r; dupi* cation will probably 
ease the storage difficulties .lonaideraLly when the praMava get 
nk^re complicated and the t-rieor;^ &rA definition lists £a^ longer, 
ji have already wriev-er. all the functiona which eheok trie differ*: sit. 
ftepL', though - c :cne cf t iir-n sr;; in <jee3 c f revision, 

After Verify fcJ 3 its satellite functions have bse.ii chs.--ked 
o'j^ .1 paan Tic wcrW 02: improving Re«hod, at the same tiins applying 
It to ehsrtra^t. aisahrii,. Ky fi^s', c'.e-. will be t-c incorporate 
nstiiro-Fteps which Hi. 11 ccrnHne several infiivJducJ atepe along with 
gpeniftj ttsQreii^ . ^kr>. t 1 £h-;ll bulla * n sac hi nary i»;hlcb allo^'t 
t rjs a "r.e p*j !: £ t e p cine .■;■? m ti a ;?"."- l£ ■ io .1*3 ^.y ill ve n> *-f or "1 np " & jv e ? the £ '.Lb - 
Htit-jt.Jona ttJght. he omitted faa 1^ ofler, dotrc ir, ths oi tat ion of a 
theorem in a le>. thesis ^ronf}. After that, I shall investigate 
various learning itierhi*r.iffiDS whi.?h raij=h^ be incorporated- ' However, 
1* ia difficult ta anUsipate a 4 : this point Just what cojra-? the 
projsei will foin&w; fh-a plan,* at cash stag* will be infl^en^ed 
sr-rsngiy fcy the rOP^Jti* of t-hu pr&ce'3in£ f.taee.